%invariante noEntranDosVeces:
(\forall x \selec SalidasDNI(h))(\forall i,j \selec ingresosDe(x,h), i \neq j) snd(i) \neq snd(j)